package de.uka.ilkd.key.dl.arithmetics.impl.metitarski;

import java.io.File;
import java.util.LinkedList;
import java.util.List;
import java.util.Properties;

import de.uka.ilkd.key.dl.options.EPropertyConstant;
import de.uka.ilkd.key.gui.GUIEvent;
import de.uka.ilkd.key.gui.configuration.Settings;
import de.uka.ilkd.key.gui.configuration.SettingsListener;
import de.uka.ilkd.key.proof.ProofSaver;

public class Options implements Settings{

	public static final Options INSTANCE = new Options();

	private File metitBinary;
	private String metitAxioms;
	
	
	/* (Pertinent) MetiTarski command-line options.

	  --time positive integer ............ processor time limit (in seconds)
	  --maxweight, -w positive integer ... maximum weight of a retained clause
	  --maxalg positive integer .......... maximum number of symbols in an algebraic clause
	  --qlimit positive integer .......... maximum number of quantified variables for QEPCAD
	  --cases #cases+weight .............. max permitted active case splits/nonSOS weighting factor in tenths (10 = neutral weighting)
	  --backtracking off/ON .............. turn backtracking off (default is on)
	  --proj_ord off/ON .................. switch CAD projection ordering off (default is on)
	  --icp_cad .......................... enable polynomial ICP before CAD
	  --icp .............................. enable only polynomial ICP, no CAD
	  --unsafe_divisors .................. omit the check for nonzero divisors
	  --full ............................. include variable instantiations in proofs
	 
	 */

	private long timeout;
	private long maxweight;
	private long maxalg;
	private long qlimit;
	private long cases;
	private boolean backtracking;
	private boolean proj_ord ;
	private boolean icp_cad ;
	private boolean icp ;
	private boolean unsafe_divisors ;
	private boolean full;


	private List<SettingsListener> listeners;

	private Options() {
		listeners = new LinkedList<SettingsListener>();
		metitBinary = new File("/opt/metit-1.9/metit");
		metitAxioms="/opt/metit-1.9/tptp/Axioms";
		timeout=-1;
		maxweight=-1;
		maxalg=-1;
		qlimit=-1;
		cases=-1;
		backtracking = true;
		proj_ord=true;
		icp_cad=false;
		icp=false;
		unsafe_divisors=false;
		full=false;
	}


	public void addSettingsListener(SettingsListener l) {
		listeners.add(l);
	}

	private void firePropertyChanged() {
		for (SettingsListener l : listeners) {
			l.settingsChanged(new GUIEvent(this));
		}
	}
	
	
	//TODO:  Metit property enums
	
	public void readSettings(Properties props) {
		String property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_BINARY.getKey());
		if (property != null) {
			metitBinary = new File(property);
		}
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_AXIOMS
						.getKey());
		if (property != null) {
			metitAxioms = property;
		}
		
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_MAXWEIGHT
						.getKey());
		if (property != null) {
			maxweight = Long.parseLong(property);
		}
		
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_MAXALG
						.getKey());
		if (property != null) {
			maxalg = Long.parseLong(property);
		}
		
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_QLIMIT
						.getKey());
		if (property != null) {
			qlimit = Long.parseLong(property);
		}
		
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_CASES
						.getKey());
		if (property != null) {
			cases = Long.parseLong(property);
		}
		
		
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_BACKTRACKING
						.getKey());
		if (property != null) {
			backtracking = Boolean.parseBoolean(property);
		}
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_PROJ_ORD
						.getKey());
		if (property != null) {
			proj_ord = Boolean.parseBoolean(property);
		}
		
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_ICP_CAD
						.getKey());
		if (property != null) {
			icp_cad = Boolean.parseBoolean(property);
		}
		
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_ICP
						.getKey());
		if (property != null) {
			icp = Boolean.parseBoolean(property);
		}
		
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_UNSAFE_DIVISORS
						.getKey());
		if (property != null) {
			unsafe_divisors = Boolean.parseBoolean(property);
		}
		property = props
				.getProperty(EPropertyConstant.METIT_OPTIONS_FULL
						.getKey());
		if (property != null) {
			full = Boolean.parseBoolean(property);
		}
		
	}


	public void writeSettings(Properties props) {
		if (!ProofSaver.isInSavingMode()) {
			props.setProperty(EPropertyConstant.METIT_OPTIONS_BINARY.getKey(),
					metitBinary.getAbsolutePath());
		}
		props.setProperty(EPropertyConstant.METIT_OPTIONS_BACKTRACKING.getKey(), ""
				+ backtracking);

	}

	// Methods as elsewhere

	public File getMetitBinary() {
		return metitBinary;
	}

	public void setMetitBinary(File metitBinary) {
		if (!this.metitBinary.equals(metitBinary)) {
			this.metitBinary = metitBinary;
			firePropertyChanged();
		}
	}
	
	public String getMetitAxioms() {
		return metitAxioms;
	}

	public void setMetitAxioms(String metitAxioms) {
		if (!this.metitAxioms.equals(metitAxioms)) {
			this.metitAxioms = metitAxioms;
			firePropertyChanged();
		}
	}

	
	/* 
	 * Option getter/setter methods.
	 * Numeric options.
	 */
	
	
	public long getTimeout() {
		return timeout;
	}

	public void setTimeout(long timeout) {
		if (this.timeout != timeout) {
			this.timeout = timeout;
			firePropertyChanged();
		}
	}
	
	
	public long getMaxalg() {
		return maxalg;
	}

	public void setMaxalg(long maxalg) {
		if (this.maxalg != maxalg) {
			this.maxalg = maxalg;
			firePropertyChanged();
		}
	}
	
	public long getMaxweight() {
		return maxweight;
	}

	public void setMaxweight(long maxweight) {
		if (this.maxweight != maxweight) {
			this.maxweight = maxweight;
			firePropertyChanged();
		}
	}
	
	
	public long getQlimit() {
		return qlimit;
	}

	public void setQlimit(long qlimit) {
		if (this.qlimit != qlimit) {
			this.qlimit = qlimit;
			firePropertyChanged();
		}
	}
	
	public long getCases() {
		return cases;
	}

	public void setCases(long cases) {
		if (this.cases != cases) {
			this.cases = cases;
			firePropertyChanged();
		}
	}
	
	/*
	 * Boolean options
	 */
	
	public boolean isProj_ord() {
		return proj_ord;
	}

	public void setProj_ord(boolean proj_ord) {
		if(this.proj_ord != proj_ord) {
			this.proj_ord = proj_ord;
			firePropertyChanged();
		}
	}	
	
	public boolean isBacktracking() {
		return backtracking;
	}

	public void setBacktracking(boolean backtracking) {
		if(this.backtracking != backtracking) {
			this.backtracking = backtracking;
			firePropertyChanged();
		}
	}	
	
	public boolean isIcp_cad() {
		return icp_cad;
	}

	public void setIcp_cad(boolean icp_cad) {
		if(this.icp_cad != icp_cad) {
			this.icp_cad = icp_cad;
			firePropertyChanged();
		}
	}	
	
	public boolean isIcp() {
		return icp;
	}

	public void setIcp(boolean icp) {
		if(this.icp != icp) {
			this.icp = icp;
			firePropertyChanged();
		}
	}	
	
	public boolean isUnsafe_divisors() {
		return unsafe_divisors;
	}

	public void setUnsafe_divisors(boolean unsafe_divisors) {
		if(this.unsafe_divisors != unsafe_divisors) {
			this.unsafe_divisors = unsafe_divisors;
			firePropertyChanged();
		}
	}	
	
	public boolean isFull() {
		return full;
	}

	public void setFull(boolean full) {
		if(this.full != full) {
			this.full = full;
			firePropertyChanged();
		}
	}	
	
}
